%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Saved with string encoding Unicode (UTF-8)



@article{Martin96b,
	Author = {Martin, Robert C},
	Date-Added = {2007-08-30 10:55:44 +0200},
	Date-Modified = {2009-05-21 13:57:00 +0200},
	Journal = {C++ Report},
	Keywords = {principles},
	Month = mar,
	Number = {3},
	Pages = {30--37},
	Title = {{The Liskov Substitution Principle}},
	Url = {http://www.objectmentor.com/publications/lsp.pdf},
	Volume = {8},
	Year = {1996}}

@inproceedings{Canning89a,
	Address = {New York, NY, USA},
	Author = {Canning, Peter and Cook, William and Hill, Walter and Olthoff, Walter and Mitchell, John C.},
	Booktitle = {Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture},
	Date-Added = {2016-02-26 15:40:31 +0000},
	Date-Modified = {2016-02-26 15:40:31 +0000},
	Doi = {10.1145/99370.99392},
	Isbn = {0-89791-328-0},
	Location = {Imperial College, London, United Kingdom},
	Pages = {273--280},
	Publisher = {ACM},
	Series = {FPCA '89},
	Title = {F-bounded Polymorphism for Object-oriented Programming},
	Url = {http://doi.acm.org/10.1145/99370.99392},
	Year = {1989}}

@techreport{ECMA15a,
	Author = {ECMA},
	Date-Added = {2015-07-14 08:18:49 +0000},
	Date-Modified = {2015-07-14 08:18:49 +0000},
	Institution = {ISO/IEC},
	Month = jun,
	Number = {ECMA-262, 6th Edition},
	Title = {{ECMAScript 2015 Language Specification}},
	Type = {International Standard},
	Url = {http://www.ecma-international.org/ecma-262/6.0/index.html},
	Year = {2015}}

@techreport{ECMA18a,
	Author = {ECMA},
	Date-Added = {2019-06-06 08:29:00 +0000},
	Date-Modified = {2019-06-06 08:29:00 +0000},
	Institution = {ISO/IEC},
	Month = jun,
	Number = {ECMA-262, 9th Edition},
	Title = {{ECMAScript 2018 Language Specification}},
	Type = {International Standard},
	Url = {http://www.ecma-international.org/ecma-262/9.0/index.html},
	Year = {2018}}

@manual{OMG14a,
	Address = {Needham, MA},
	Author = {OMG},
	Date-Added = {2015-07-14 08:17:57 +0000},
	Date-Modified = {2015-07-14 08:17:57 +0000},
	Edition = {formal/2014-03-01, version 3.5},
	Importance = {5},
	Keywords = {Corba, IDL},
	Month = mar,
	Organization = {Object Management Group},
	Printed = {Yes},
	Rating = {5},
	Title = {{Interface Definition Language}},
	Url = {http://www.omg.org/cgi-bin/doc?formal/2014-03-01.pdf},
	Year = {2014},
	Abstract = {This Request for Proposal (RFP) is one of a series of RFPs related to
developing the next major revision of the OMG Meta Object Facility
specification, which will be referred to as MOF 2.0. Some of the RFPs
pertain to specifying the technology neutral MOF itself, while others
pertain to mapping the MOF to specific implementation technologies.
This RFP addresses a technology neutral part of MOF and pertains to:
1. Queries on models.
2. Views on metamodels.
3. Transformations of models. }}

@book{Gosling15a,
	Author = {Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad and Buckley, Alex},
	Booktitle = {The Java Language Specification. Java SE 8 Edition},
	Date-Added = {2015-07-14 08:17:57 +0000},
	Date-Modified = {2016-02-14 16:38:02 +0000},
	Edition = {JSR-337 Java® SE 8 Release Contents},
	Month = feb,
	Publisher = {Oracle},
	Title = {The Java Language Specification. Java SE 8 Edition},
	Url = {http://docs.oracle.com/javase/specs/jls/se8/jls8.pdf},
	Year = {2015}}

@techreport{W3C:Steen:14:XL,
	Author = {Steen, Hallvord and Aubourg, Julian and van Kesteren, Anne and Song, Jungkee},
	Bibsource = {http://w2.syronex.com/jmr/w3c-biblio},
	Date-Added = {2015-07-14 08:17:57 +0000},
	Date-Modified = {2015-07-14 08:17:57 +0000},
	Institution = {W3C},
	Keywords = {W3C},
	Month = jan,
	Note = {http://www.w3.org/TR/2014/WD-XMLHttpRequest-20140130/},
	Title = {{XMLHttpRequest} Level 1},
	Type = {{W3C} Working Draft},
	Year = {2014}}

@misc{Kuizinas14a,
	Author = {Kuizinas, Gajus},
	Date-Added = {2015-07-14 08:17:57 +0000},
	Date-Modified = {2015-07-14 08:17:57 +0000},
	Month = oct,
	Title = {The Definitive Guide to the JavaScript Generators},
	Url = {http://gajus.com/blog/2/the-definetive-guide-to-the-javascript-generators},
	Year = {2014}}

@techreport{W3C12a,
	Author = {W3C},
	Date-Added = {2015-07-14 08:17:57 +0000},
	Date-Modified = {2015-07-14 08:17:57 +0000},
	Institution = {W3C},
	Month = apr,
	Number = {19 April 2012},
	Title = {{Web IDL Specification}},
	Type = {W3C Candidate Recommendation},
	Url = {http://www.w3.org/TR/2012/CR-WebIDL-20120419/},
	Year = {2012}}

@inproceedings{Cook90a,
	Address = {New York, NY, USA},
	Author = {Cook, William R. and Hill, Walter and Canning, Peter S.},
	Booktitle = {Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
	Date-Added = {2015-07-14 08:17:57 +0000},
	Date-Modified = {2015-07-14 08:17:57 +0000},
	Doi = {10.1145/96709.96721},
	Isbn = {0-89791-343-4},
	Location = {San Francisco, California, USA},
	Pages = {125--135},
	Publisher = {ACM},
	Series = {POPL '90},
	Title = {Inheritance is Not Subtyping},
	Year = {1990}}

@book{Knol13a,
	Author = {Knol, Alex},
	Booktitle = {Dependency injection with AngularJS},
	Date-Added = {2015-07-14 08:10:08 +0000},
	Date-Modified = {2015-07-14 08:10:08 +0000},
	Isbn = {987-1-78216-656-6},
	Keywords = {dependency injection},
	Month = dec,
	Publisher = {Packt Publishing},
	Title = {Dependency injection with AngularJS},
	Year = {2013}}

@book{Betts13a,
	Author = {Betts, Dominic and Melnik, Grigori and Simonazzi, Fernando and Subramanian, Mani},
	Date-Added = {2015-07-14 08:10:08 +0000},
	Date-Modified = {2015-07-14 08:10:08 +0000},
	Edition = {1st},
	Isbn = {978-1-6211-4028-3},
	Keywords = {dependency injection},
	Publisher = {Microsoft patterns and practices},
	Title = {Dependency Injection with Unity},
	Year = {2013}}

@misc{Lesiecki08a,
	Author = {Lesiecki, Nicholas},
	Date-Added = {2015-07-14 08:10:08 +0000},
	Date-Modified = {2015-07-14 08:10:08 +0000},
	Keywords = {dependency injection},
	Month = dec,
	Printed = {1},
	Title = {Dependency injection with Guice},
	Url = {http://www.ibm.com/developerworks/library/j-guice/},
	Year = {2008}}

@book{Prasanna09a,
	Author = {Prasanna, Dhanji R},
	Booktitle = {Dependency Injection: Design Patterns Using Spring and Guice},
	Date-Added = {2015-07-14 08:09:09 +0000},
	Date-Modified = {2015-07-14 08:09:09 +0000},
	Isbn = {987-1-933988-55-8},
	Keywords = {dependency injection},
	Publisher = {Manning Publications},
	Title = {Dependency Injection: Design Patterns Using Spring and Guice},
	Year = {2009}}

@misc{Fowler04b,
	Author = {Fowler, Martin},
	Date-Added = {2015-07-14 08:09:09 +0000},
	Date-Modified = {2015-07-14 08:09:09 +0000},
	Keywords = {dependency injection},
	Month = jan,
	Printed = {1},
	Title = {Inversion of Control Containers and the Dependency Injection pattern},
	Url = {http://martinfowler.com/articles/injection.html},
	Year = {2004}}

@inproceedings{Zhu13a,
	Author = {Zhu, He and Jagannathan, Suresh},
	Booktitle = {Verification, Model Checking, and Abstract Interpretation},
	Date-Added = {2015-07-14 08:07:03 +0000},
	Date-Modified = {2015-07-14 08:09:17 +0000},
	Editor = {Giacobazzi, Roberto and Berdine, Josh and Mastroeni, Isabella},
	Isbn = {978-3-642-35872-2},
	Keywords = {dependency injection},
	Pages = {295-314},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Compositional and Lightweight Dependent Type Inference for ML},
	Url = {https://doi.org/10.1007/978-3-642-35873-9_19},
	Volume = {7737},
	Year = {2013}}

@article{Hudli13a,
	Author = {Hudli, Shrinidhi R. and Hudli, Raghu V.},
	Date-Added = {2015-07-14 08:07:03 +0000},
	Date-Modified = {2015-07-14 08:09:17 +0000},
	Doi = {10.7763/LNSE.2013.V1.16},
	Issn = {2301-3559},
	Journal = {Lecture Notes on Software Engineering},
	Keywords = {dependency injection},
	Number = {1},
	Pages = {71--74},
	Title = {A Verification Strategy for Dependency Injection},
	Volume = {1},
	Year = {2013},
	Abstract = {Dependency Injection (DI) is a powerful design and implementation technique to create designs that result in loosely coupled classes in object-oriented environments. IOC containers such as Spring provide a framework to describe the DI constructs for classes that have been designed with dependency inversion. However the knowledge of classes and their dependency is now distributed between the code and context files where the wiring of the classes (beans) is specified.
While IOC containers are able to automatically inject dependent objects at run time based on wiring descriptions, programmers often have the tedious job of ensuring that the wiring descriptions are type safe and will not result in runtime exceptions.
We propose an object reflection driven approach to provide DI verification based on static analysis of the classes that have dependency inversion and their wiring descriptions.}}

@inproceedings{Smith08a,
	Address = {New York, NY, USA},
	Author = {Smith, Daniel and Cartwright, Robert},
	Booktitle = {Proceedings of the 23rd ACM SIGPLAN Conference on Object-oriented Programming Systems Languages and Applications},
	Date-Added = {2013-12-06 17:44:28 +0000},
	Date-Modified = {2013-12-06 17:44:28 +0000},
	Doi = {10.1145/1449764.1449804},
	Isbn = {978-1-60558-215-3},
	Keywords = {type system},
	Location = {Nashville, TN, USA},
	Pages = {505--524},
	Publisher = {ACM},
	Series = {OOPSLA '08},
	Title = {Java Type Inference is Broken: Can We Fix It?},
	Year = {2008}}

@manual{King13a,
	Author = {King, Gavin},
	Booktitle = {The Ceylon Language},
	Date-Added = {2013-11-19 18:31:26 +0000},
	Date-Modified = {2013-11-19 18:31:26 +0000},
	Edition = {1.0},
	Organization = {Red Hat, Inc.},
	Title = {The Ceylon Language},
	Url = {http://ceylon-lang.org/documentation/1.0/spec/pdf/ceylon-language-specification.pdf},
	Year = {2013}}

@inproceedings{Bak02a,
	Author = {Bak, Lars and Bracha, Gilad and Grarup, Steffen and Griesemer, Robert and Griswold, David and Hoelzle, Urs},
	Booktitle = {ECOOP02 Workshop on Inheritance},
	Date-Added = {2013-11-19 18:31:26 +0000},
	Date-Modified = {2013-11-19 18:31:26 +0000},
	Month = jun,
	Title = {Mixins in Strongtalk},
	Url = {http://www.bracha.org/mixins-paper.pdf},
	Year = {2002}}

@techreport{OSGi-Alliance13a,
	Author = {{OSGi Alliance}},
	Date-Added = {2013-10-21 12:51:59 +0000},
	Date-Modified = {2013-10-21 12:51:59 +0000},
	Institution = {The OSGi Alliance},
	Month = jul,
	Number = {RFP 159},
	Title = {JavaScript Microservices},
	Type = {RFP},
	Url = {https://www.osgi.org/bugzilla/show_bug.cgi?id=169},
	Year = {2013}}

@techreport{OSGi-Alliance11a,
	Author = {{OSGi Alliance}},
	Date-Added = {2013-10-21 12:51:59 +0000},
	Date-Modified = {2013-10-21 12:51:59 +0000},
	Institution = {The OSGi Alliance},
	Number = {Release 4, Version 4.3},
	Title = {OSGi Service Platform Core Specification},
	Type = {Specification},
	Url = {http://www.osgi.org/download/r4v43/osgi.core-4.3.0.pdf},
	Year = {2011}}

@inproceedings{Nielson99a,
	Author = {Nielson, Flemming and Nielson, HanneRiis},
	Booktitle = {Correct System Design},
	Date-Added = {2013-09-24 13:39:25 +0000},
	Date-Modified = {2013-09-24 13:39:25 +0000},
	Editor = {Olderog, Ernst-Rüdiger and Steffen, Bernhard},
	Isbn = {978-3-540-66624-0},
	Keywords = {Polymorphic type systems; effect annotations; subeffecting and subtyping; semantic correctness; type inference algorithms; syntactic soundness and completeness; Analyses for control flow; binding times; side effects; region structure; communication structure},
	Language = {English},
	Pages = {114-136},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Type and Effect Systems},
	Url = {https://doi.org/10.1007/3-540-48092-7_6},
	Volume = {1710},
	Year = {1999}}

@article{Laurent12a,
	Author = {Laurent, Olivier},
	Date-Added = {2013-09-18 08:19:40 +0000},
	Date-Modified = {2013-09-18 08:19:40 +0000},
	Title = {Intersection types with subtyping by means of cut elimination},
	Year = {2012}}

@article{Igarashi07a,
	Author = {Igarashi, Atsushi and Nagira, Hideshi},
	Date-Added = {2013-09-18 07:25:39 +0000},
	Date-Modified = {2013-09-18 07:25:39 +0000},
	Journal = {Journal of Object Technology},
	Number = {2},
	Title = {Union Types for Object-Oriented Programming},
	Url = {http://www.jot.fm/issues/issue_2007_02/article3/},
	Volume = {6},
	Year = {2007}}

@url{MozillaJSRef,
	Date-Added = {2013-09-10 14:16:05 +0000},
	Date-Modified = {2013-09-10 14:17:24 +0000},
	Title = {JavaScript Reference},
	Url = {https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference}}

@article{West06a,
	Author = {West, Mike},
	Date-Added = {2013-09-10 14:14:46 +0000},
	Date-Modified = {2013-09-10 14:14:46 +0000},
	Journal = {Digital Web Magazine},
	Month = sep,
	Title = {Scope in JavaScript},
	Url = {http://www.digital-web.com/articles/scope_in_javascript/},
	Year = {2006}}

@techreport{Scharli02a,
	Author = {Schärli, Nathanael and Ducasse, Stéphane and Nierstraszand, Oscar and Black, Andrew},
	Date-Added = {2013-07-22 15:04:35 +0000},
	Date-Modified = {2013-07-22 15:53:15 +0000},
	Institution = {Universität Bern, Institut für Informatik und angewandte Mathematik},
	Month = nov,
	Number = {IAM-02-005},
	Title = {Traits: Composable Units of Behavior},
	Type = {Technical Report},
	Url = {http://scg.unibe.ch/archive/papers/Scha02bTraits.pdf},
	Year = {2002}}

@manual{Dart13a,
	Author = {{{Dart} Team}},
	Booktitle = {Dart Programming Language Specification},
	Date-Added = {2013-07-17 14:47:11 +0000},
	Date-Modified = {2013-11-14 13:47:42 +0000},
	Edition = {1.0},
	Month = jun,
	Title = {Dart Programming Language Specification},
	Url = {http://www.dartlang.org/docs/spec/latest/dart-language-specification.pdf},
	Year = {2013}}

@techreport{ECMA13a,
	Date-Added = {2013-05-27 13:59:39 +0000},
	Date-Modified = {2013-05-27 13:59:39 +0000},
	Institution = {ISO/IEC},
	Month = may,
	Number = {ECMA-262, 6th Edition, May 14, 2013},
	Title = {{Draft ECMAScript Language Specification}},
	Type = {Working Draft},
	Url = {http://wiki.ecmascript.org/doku.php?id=harmony:specification_drafts},
	Year = {2013}}

@manual{Xtext24,
	Author = {{Xtext Team}},
	Booktitle = {Xtext 2.4 Documentation},
	Date-Added = {2013-05-27 13:59:39 +0000},
	Date-Modified = {2013-05-27 13:59:39 +0000},
	Month = apr,
	Organization = {Eclipse Foundation},
	Title = {Xtext 2.4 Documentation},
	Url = {http://www.eclipse.org/Xtext/documentation/2.4.0/Documentation.pdf},
	Year = {2013}}

@inproceedings{Wehr08a,
	Address = {Paphos, Cyprus},
	Author = {Wehr, Stefan and Thiemann, Peter},
	Booktitle = {10th Workshop on Formal Techniques for {Java}-like Programs {FTfJP} 2008, informal proceedings},
	Date-Added = {2013-05-15 15:42:36 +0000},
	Date-Modified = {2013-05-15 15:42:36 +0000},
	Title = {Subtyping Existential Types},
	Url = {http://www.stefanwehr.de/publications/Wehr_Subtyping_existential_types.pdf},
	Year = 2008,
	Abstract = {Constrained existential types are a powerful language feature that subsumes Java-like interface and wildcard types. But existentials do not mingle well with subtyping: subtyping is already undecidable for very restrictive settings. This paper defines two subtyping relations by extracting the features specific to existentials from current language proposals (JavaGI, WildFJ, Scala). Both subtyping relations are undecidable. The paper also discusses the consequences of removing existentials from JavaGI and possible amendments to regain their features.
}}

@inproceedings{Cameron07a,
	Author = {Cameron, Nicholas and Ernst, Erik and Drossopoulou, Sophia},
	Booktitle = {Formal Techniques for Java-like Programs (FTfJP) 2007},
	Date-Added = {2013-05-15 15:39:14 +0000},
	Date-Modified = {2013-05-15 15:39:14 +0000},
	Month = {July},
	Title = {{Towards an Existential Types Model for Java Wildcards}},
	Url = {http://pubs.doc.ic.ac.uk/towards-existential-wildcards/},
	Year = {2007},
	Abstract = {Wildcards extend Java generics by softening the mismatch between subtype and parametric polymorphism. Although they are a key part of the Java 5.0 programming language, a type system including wildcards has never been proven type sound. Wildcards have previously been formalised as existential types. In this paper we extend FGJ, a featherweight formalisation of Java with generics, with existential types. We prove that this calculus, ExistsJ, is type sound, and illustrate how it models wildcards in the Java Programming Language. ExistsJ is not a full model for Java wildcards, because it does not support lower bounds for wildcards. We discuss why ExistsJ can not be easily extended with lower bounds, and how full Java wildcards could be modelled in a type sound way.
}}

@phdthesis{Cameron09a,
	Author = {Cameron, Nicholas},
	Date-Added = {2013-05-15 14:40:27 +0000},
	Date-Modified = {2013-11-20 12:50:08 +0000},
	Month = apr,
	School = {University of London; Imperial College, Department of Computing},
	Title = {Existential Types for Variance -- Java Wildcards and Ownership Types},
	Type = {PhD Thesis},
	Url = {http://www.doc.ic.ac.uk/~ncameron/papers/cameron_thesis.pdf},
	Year = {2009}}

@inproceedings{Summers10a,
	Acmid = {1924522},
	Address = {New York, NY, USA},
	Articleno = {2},
	Author = {Summers, Alexander J. and Cameron, Nicholas and Dezani-Ciancaglini, Mariangiola and Drossopoulou, Sophia},
	Booktitle = {Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs},
	Date-Added = {2013-05-15 14:22:22 +0000},
	Date-Modified = {2013-06-27 09:44:55 +0000},
	Doi = {10.1145/1924520.1924522},
	Isbn = {978-1-4503-0540-2},
	Location = {Maribor, Slovenia},
	Numpages = {7},
	Pages = {2:1--2:7},
	Publisher = {ACM},
	Rating = {4},
	Series = {FTFJP '10},
	Title = {Towards a semantic model for Java wildcards},
	Year = {2010},
	Abstract = {Wildcard types enrich the types expressible in Java, and extend the set of typeable Java programs. Syntactic models and proofs of soundness for type systems related to Java wildcards have been suggested in the past, however, the semantics of wildcards has not yet been studied.

In this paper we propose a semantic model for Java wildcards, inspired by work on semantic subtyping, which traditionally interprets types as sets of possible values. To easily reflect the nominal type system of Java, our model is defined in terms of runtime types (closed class types) rather than the structure of the runtime values themselves. To reflect the variance introduced by wildcards, our model interprets types as sets of such closed class types.

Having defined our model, we employ a standard semantic notion of subtyping. We show soundness of syntactic subtyping with respect to the semantic version, and demonstrate that completeness fails in the general case. We identify a restricted (but nonetheless rich) type language for which the syntactic notion of subtyping is both sound and complete.}}

@inproceedings{Cameron08b,
	Author = {Cameron, Nicholas and Drossopoulou, Sophia and Ernst, Erik},
	Booktitle = {ECOOP 2008 -- Object-Oriented Programming},
	Date-Added = {2013-05-15 14:15:51 +0000},
	Date-Modified = {2013-05-15 14:22:44 +0000},
	Editor = {Vitek, Jan},
	Isbn = {978-3-540-70591-8},
	Pages = {2-26},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {A Model for Java with Wildcards},
	Url = {https://doi.org/10.1007/978-3-540-70592-5_2},
	Volume = {5142},
	Year = {2008},
	Abstract = {Wildcards are a complex and subtle part of the Java type system, present since version 5.0. Although there have been various formalisations and partial type soundness results concerning wildcards, to the best of our knowledge, no system that includes all the key aspects of Java wildcards has been proven type sound. This paper establishes that Java wildcards are type sound. We describe a new formal model based on explicit existential types whose pack and unpack operations are handled implicitly, and prove it type sound. Moreover, we specify a translation from a subset of Java to our formal model, and discuss how several interesting aspects of the Java type system are handled.
}}

@techreport{Schwartzbach97a,
	Address = {Arhus, DK},
	Author = {Schwartzbach, Michael I.},
	Date-Added = {2013-05-08 13:15:03 +0000},
	Date-Modified = {2013-05-08 13:15:03 +0000},
	Institution = {Department of Computer Science University of Aarhus},
	Month = may,
	Title = {Object-Oriented Type Systems. Principles and Applications},
	Type = {Efteruddannelseskursus for Datamatikerlaererforeningen},
	Url = {http://cs.au.dk/~mis/ootspa.ps},
	Year = {1997}}

@techreport{Flatt99a,
	Author = {Flatt, Matthew and Krishnamurthi, Shriram and Felleisen, Matthias},
	Date-Added = {2013-05-08 13:14:48 +0000},
	Date-Modified = {2013-11-20 12:49:22 +0000},
	Institution = {Rice University},
	Month = jun,
	Number = {TR 97-293},
	Title = {A Programmer's Reduction Semantics for Classes and Mixins},
	Type = {Technical Report},
	Url = {http://www.ccs.neu.edu/racket/pubs/tr97-293.pdf},
	Year = {1999}}

@inproceedings{Torgersen05a,
	Address = {California, US},
	Author = {Torgersen, Mads and Ernst, Erik and Hansen, Christian Plesner},
	Booktitle = {Foundations of Object-Oriented Languages (FOOL 2005)},
	Date-Added = {2013-05-07 12:32:04 +0000},
	Date-Modified = {2013-05-07 12:32:04 +0000},
	Month = jan,
	Title = {Wild FJ},
	Url = {http://homepages.inf.ed.ac.uk/wadler/fool/program/14.html},
	Year = {2005},
	Abstract = {This paper presents a formalization of wildcards, which is one of the new features of the Java programming language in version JDK5.0. Wildcards help alleviating the impedance mismatch between generics, or parametric polymorphism, and traditional object-oriented subtype polymorphism. They do this by quantifying over parameterized types with different type arguments. Wildcards take inspiration from several sources including use-site variance, and they could be considered as a way to introduce a syntactically light-weight and not fully general kind of existential types into a main-stream language. This formalization describes the approach, in particular the wildcard capture process where the existential nature of wildcards becomes evident.
}}

@inproceedings{Altidor12a,
	Affiliation = {University of Massachusetts, Amherst, USA},
	Author = {Altidor, John and Reichenbach, Christoph and Smaragdakis, Yannis},
	Booktitle = {ECOOP 2012 -- Object-Oriented Programming},
	Date-Added = {2013-04-19 11:55:54 +0000},
	Date-Modified = {2013-05-27 14:50:37 +0000},
	Doi = {10.1007/978-3-642-31057-7_23},
	Editor = {Noble, James},
	Isbn = {978-3-642-31056-0},
	Keyword = {generics},
	Keywords = {generics},
	Pages = {509-534},
	Publisher = {Springer},
	Rating = {4},
	Series = {Lecture Notes in Computer Science},
	Title = {Java Wildcards Meet Definition-Site Variance},
	Volume = {7313},
	Year = {2012},
	Abstract = {Variance is concerned with the interplay of parametric polymorphism (i.e., templates, generics) and subtyping. The study of variance gives answers to the question of when an instantiation of a generic class can be a subtype of another. In this work, we combine the mechanisms of use-site variance (as in Java) and definition-site variance (as in Scala and C#) in a single type system, based on Java. This allows maximum flexibility in both the specification and use of generic types, thus increasing the reusability of code. Our VarJ calculus achieves a safe synergy of def-site and use-site variance, while supporting the full complexities of the Java realization of variance, including F-bounded polymorphism and wildcard capture. We show that the interaction of these features with definition-site variance is non-trivial and offer a full proof of soundness---the first in the literature for an approach combining variance mechanisms.}}

@manual{Joose,
	Author = {Platonov, Nickolay},
	Booktitle = {{joose.github.com/Joose/doc/html/Joose/Manual.html, Project Website}},
	Date-Added = {2013-04-18 12:57:37 +0000},
	Date-Modified = {2013-04-18 12:58:33 +0000},
	Key = {Joose},
	Lastchecked = {2013-03-21},
	Title = {Joose Manual},
	Url = {http://joose.github.com/Joose/doc/html/Joose/Manual.html},
	Year = {2013}}

@article{Crary02a,
	Author = {Crary, Karl and Weirich, Stephanie and Morrisett, Greg},
	Date-Added = {2013-04-17 15:59:29 +0000},
	Date-Modified = {2013-04-17 15:59:29 +0000},
	Doi = {10.1017/S0956796801004282},
	Issn = {1469-7653},
	Issue = {06},
	Journal = {Journal of Functional Programming},
	Month = {10},
	Numpages = {34},
	Pages = {567--600},
	Title = {Intensional polymorphism in type-erasure semantics},
	Url = {http://journals.cambridge.org/article_S0956796801004282},
	Volume = {12},
	Year = {2002},
	Abstract = {Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling and attened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks: it requires duplication of run-time constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion. We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place, thereby avoiding certain beta-expansions required by other frameworks.
}}

@booklet{Aehlig01a,
	Author = {Aehlig, Klaus and Fischbacher, Thomas},
	Date-Added = {2013-03-15 10:22:46 +0000},
	Date-Modified = {2013-03-15 10:26:17 +0000},
	Howpublished = {Script des Lambda-Kalkül-Kurses, CdE-Pfingstakademie},
	Title = {{Einführung in den $\lambda$-Kalkül}},
	Url = {http://www.southampton.ac.uk/~doctom/teaching/lambda},
	Year = {2001}}

@incollection{Spoon04a,
	Author = {Spoon, S.Alexander and Shivers, Olin},
	Booktitle = {ECOOP 2004 -- Object-Oriented Programming},
	Date-Added = {2013-03-12 16:55:50 +0000},
	Date-Modified = {2013-03-12 16:56:07 +0000},
	Doi = {10.1007/978-3-540-24851-4_3},
	Editor = {Odersky, Martin},
	Isbn = {978-3-540-22159-3},
	Pages = {51-74},
	Publisher = {Springer Berlin Heidelberg},
	Series = {Lecture Notes in Computer Science},
	Title = {Demand-Driven Type Inference with Subgoal Pruning: Trading Precision for Scalability},
	Url = {https://doi.org/10.1007/978-3-540-24851-4_3},
	Volume = {3086},
	Year = {2004},
	Abstract = {downloaded from http://lexspoon.org/chuck/spoon-ecoop04.pdf}}

@techreport{Spoon06a,
	Author = {Spoon, Alexander S. and Shivers, Olin},
	Date-Added = {2013-03-12 15:09:12 +0000},
	Date-Modified = {2013-03-12 15:10:37 +0000},
	Month = mar,
	Number = {revision 1639},
	Title = {Demand-Driven Type Inference with Subgoal Pruning},
	Url = {http://lexspoon.org/chuck/ddp.pdf},
	Year = {2006},
	Abstract = {Type Inference Algorithm mentioned in the DLTK proposal}}

@inproceedings{Oxhoj92a,
	Acmid = {679213},
	Address = {London, UK, UK},
	Author = {Oxhøj, Nicholas and Palsberg, Jens and Schwartzbach, Michael I.},
	Booktitle = {Proceedings of the European Conference on Object-Oriented Programming},
	Date-Added = {2013-03-11 15:56:49 +0000},
	Date-Modified = {2013-03-11 15:57:12 +0000},
	Isbn = {3-540-55668-0},
	Numpages = {21},
	Pages = {329--349},
	Publisher = {Springer-Verlag},
	Series = {ECOOP '92},
	Title = {Making Type Inference Practical},
	Url = {http://dl.acm.org/citation.cfm?id=646150.679213},
	Year = {1992},
	Annote = {doc from http://www.cs.ucla.edu/~palsberg/paper/ecoop92.pdf}}

@inproceedings{Palsberg91a,
	Acmid = {117965},
	Address = {New York, NY, USA},
	Author = {Palsberg, Jens and Schwartzbach, Michael I.},
	Booktitle = {Conference proceedings on Object-oriented programming systems, languages, and applications},
	Date-Added = {2013-03-11 15:52:44 +0000},
	Date-Modified = {2013-03-11 15:53:08 +0000},
	Doi = {10.1145/117954.117965},
	Isbn = {0-201-55417-8},
	Location = {Phoenix, Arizona, USA},
	Numpages = {16},
	Pages = {146--161},
	Publisher = {ACM},
	Series = {OOPSLA '91},
	Title = {Object-oriented type inference},
	Year = {1991},
	Annote = {paper from http://www.cs.ucla.edu/~palsberg/paper/oopsla91.pdf}}

@phdthesis{Anderson06a,
	Author = {Anderson, Christopher},
	Date-Added = {2013-03-11 14:49:47 +0000},
	Date-Modified = {2013-03-11 14:50:46 +0000},
	Month = mar,
	School = {Department of Computing, Imperial College London},
	Title = {Type Inference for JavaScript},
	Type = {PhD Thesis},
	Url = {http://slurp.doc.ic.ac.uk/publications/chrisandersonphd},
	Year = {2006}}

@inproceedings{Anderson05a,
	Acmid = {2144917},
	Address = {Berlin, Heidelberg},
	Author = {Anderson, Christopher and Giannini, Paola and Drossopoulou, Sophia},
	Booktitle = {Proceedings of the 19th European conference on Object-Oriented Programming},
	Date-Added = {2013-03-11 14:22:40 +0000},
	Date-Modified = {2013-03-11 14:22:43 +0000},
	Doi = {10.1007/11531142_19},
	Isbn = {3-540-27992-X, 978-3-540-27992-1},
	Location = {Glasgow, UK},
	Numpages = {25},
	Pages = {428--452},
	Publisher = {Springer-Verlag},
	Series = {ECOOP'05},
	Title = {Towards type inference for javascript},
	Url = {https://doi.org/10.1007/11531142_19},
	Year = {2005}}

@inproceedings{Jensen09a,
	Acmid = {1615460},
	Address = {Berlin, Heidelberg},
	Author = {Jensen, Simon Holm and Møller, Anders and Thiemann, Peter},
	Booktitle = {Proceedings of the 16th International Symposium on Static Analysis},
	Date-Added = {2013-03-11 14:15:47 +0000},
	Date-Modified = {2013-03-11 16:02:54 +0000},
	Doi = {10.1007/978-3-642-03237-0_17},
	Importance = {2},
	Isbn = {978-3-642-03236-3},
	Location = {Los Angeles, CA},
	Numpages = {18},
	Pages = {238--255},
	Publisher = {Springer-Verlag},
	Series = {SAS '09},
	Title = {Type Analysis for JavaScript},
	Url = {https://doi.org/10.1007/978-3-642-03237-0_17},
	Year = {2009}}

@book{Volter13a,
	Author = {Völter, Markus},
	Booktitle = {DSL Engineering. Designing, Implementing and Using Domain-Specific Languages},
	Date-Added = {2013-02-26 13:13:20 +0000},
	Date-Modified = {2013-02-26 13:14:09 +0000},
	Title = {DSL Engineering. Designing, Implementing and Using Domain-Specific Languages},
	Url = {http://dslbook.org},
	Year = {2013}}

@inproceedings{Bracha98a,
	Acmid = {286957},
	Address = {New York, NY, USA},
	Author = {Bracha, Gilad and Odersky, Martin and Stoutamire, David and Wadler, Philip},
	Booktitle = {Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1145/286936.286957},
	Isbn = {1-58113-005-8},
	Keywords = {type system},
	Location = {Vancouver, British Columbia, Canada},
	Pages = {183--200},
	Publisher = {ACM},
	Series = {OOPSLA '98},
	Title = {Making the future safe for the past: adding genericity to the Java programming language},
	Url = {http://doi.acm.org/10.1145/286936.286957},
	Year = {1998},
	Abstract = {We present GJ, a design that extends the Java programming language with generic types and methods. These are both explained and implemented by translation into the unextended language. The translation closely mimics the way generics are emulated by programmers: it erases all type parameters, maps type variables to their bounds, and inserts casts where needed. Some subtleties of the translation are caused by the handling of overriding.GJ increases expressiveness and safety: code utilizing generic libraries is no longer buried under a plethora of casts, and the corresponding casts inserted by the translation are guaranteed to not fail.GJ is designed to be fully backwards compatible with the current Java language, which simplifies the transition from non-generic to generic programming. In particular, one can retrofit existing library classes with generic interfaces without changing their code.An implementation of GJ has been written in GJ, and is freely available on the web.
}}

@incollection{Cameron08a,
	Affiliation = {Imperial College London},
	Author = {Cameron, Nicholas and Drossopoulou, Sophia and Ernst, Erik},
	Booktitle = {ECOOP 2008 -- Object-Oriented Programming},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1007/978-3-540-70592-5_2},
	Editor = {Vitek, Jan},
	Isbn = {978-3-540-70591-8},
	Keyword = {Computer Science},
	Keywords = {type system},
	Pages = {2-26},
	Publisher = {Springer Berlin / Heidelberg},
	Series = {Lecture Notes in Computer Science},
	Title = {A Model for Java with Wildcards},
	Volume = {5142},
	Year = {2008},
	Abstract = {Wildcards are a complex and subtle part of the Java type system, present since version 5.0. Although there have been various formalisations and partial type soundness results concerning wildcards, to the best of our knowledge, no system that includes all the key aspects of Java wildcards has been proven type sound. This paper establishes that Java wildcards are type sound. We describe a new formal model based on explicit existential types whose pack and unpack operations are handled implicitly, and prove it type sound. Moreover, we specify a translation from a subset of Java to our formal model, and discuss how several interesting aspects of the Java type system are handled.}}

@inproceedings{Craciun09a,
	Affiliation = {Durham University Department of Computer Science UK},
	Author = {Craciun, Florin and Chin, Wei-Ngan and He, Guanhua and Qin, Shengchao},
	Booktitle = {Programming Languages and Systems},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1007/978-3-642-00590-9_9},
	Editor = {Castagna, Giuseppe},
	Isbn = {978-3-642-00589-3},
	Keyword = {Computer Science},
	Keywords = {type system},
	Pages = {112-127},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {An Interval-Based Inference of Variant Parametric Types},
	Volume = {5502},
	Year = {2009},
	Abstract = {Variant parametric types represent the successful integration of subtype and parametric polymorphism to support a more flexible subtyping for Java like languages. A key feature that helps strengthen this integration is the use-site variance. Depending on how the fields are used, each variance denotes a covariant, a contravariant, an invariant or a bivariant subtyping. By annotating variance properties on each type argument to a parametric class, programmers can choose various desirable variance properties for each use of the parametric class. Although Java library classes have been successfully refactored to use variant parametric types, these mechanisms are often criticized, due to the difficulty of choosing appropriate variance annotations. Several algorithms have been proposed for automatically refactoring legacy Java code to use generic libraries, but none can support the full flexibility of the use-site variance-based subtyping. This paper addresses this difficulty by proposing a novel interval-based approach to inferring both the variance annotations and the type arguments. Each variant parametric type is regarded as an interval type with two type bounds, a lower bound for writing and an upper bound for reading. We propose a constraint-based inference algorithm that works on a per method basis, as a summary-based analysis.}}

@inproceedings{Ernst06b,
	Affiliation = {Department of Computer Science, University of Aarhus, Denmark},
	Author = {Ernst, Erik},
	Booktitle = {Modular Programming Languages},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1007/11860990_5},
	Editor = {Lightfoot, David and Szyperski, Clemens},
	Isbn = {978-3-540-40927-4},
	Keyword = {Computer Science},
	Keywords = {type system},
	Pages = {57-72},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Reconciling Virtual Classes with Genericity},
	Volume = {4228},
	Year = {2006}}

@inproceedings{Igarashi00a,
	Affiliation = {University of Tokyo Department of Information Science 7-3-1 Hongo, Bunkyo-ku Tokyo 113-0033 Japan},
	Author = {Igarashi, Atsushi and Pierce, Benjamin},
	Booktitle = {ECOOP 2000 --- Object-Oriented Programming},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1007/3-540-45102-1_7},
	Editor = {Bertino, Elisa},
	Isbn = {978-3-540-67660-7},
	Keyword = {Computer Science},
	Keywords = {type system},
	Pages = {129-153},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {On Inner Classes},
	Volume = {1850},
	Year = {2000},
	Abstract = {Inner classes in object-oriented languages play a role similar to nested function definitions in functional languages, allowing an object to export other objects with direct access to its own methods and instance variables. However, the similarity is deceptive: a close look at inner classes reveals significant subtleties arising from their interactions with inheritance. The goal of this work is a precise understanding of the essential features of inner classes; our object of study is a fragment of Java with inner classes and inheritance (and almost nothing else). We begin by giving a direct reduction semantics for this language. We then give an alternative semantics by translation into a yet smaller language with only top-level classes, closely following Java's Inner Classes Specfication. We prove that the two semantics coincide, in the sense that translation commutes with reduction, and that both are type-safe.}}

@article{Igarashi01a,
	Address = {New York, NY, USA},
	Author = {Igarashi, Atsushi and Pierce, Benjamin C. and Wadler, Philip},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1145/503502.503505},
	Issn = {0164-0925},
	Issue_Date = {May 2001},
	Journal = {ACM Trans. Program. Lang. Syst.},
	Keywords = {language design; type system},
	Month = may,
	Number = {3},
	Pages = {396--450},
	Publisher = {ACM},
	Title = {Featherweight Java: a minimal core calculus for Java and GJ},
	Volume = {23},
	Year = {2001},
	Abstract = {Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.
}}

@article{Igarashi06a,
	Address = {New York, NY, USA},
	Author = {Igarashi, Atsushi and Viroli, Mirko},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1145/1152649.1152650},
	Issn = {0164-0925},
	Issue_Date = {September 2006},
	Journal = {ACM Trans. Program. Lang. Syst.},
	Keywords = {language design; type system},
	Month = sep,
	Number = {5},
	Pages = {795--847},
	Publisher = {ACM},
	Title = {Variant parametric types: A flexible subtyping scheme for generics},
	Volume = {28},
	Year = {2006},
	Abstract = {We develop the mechanism of variant parametric types as a means to enhance synergy between parametric and inclusion polymorphism in object-oriented programming languages. Variant parametric types are used to control both the subtyping between different instantiations of one generic class and the accessibility of their fields and methods. On one hand, one parametric class can be used to derive covariant types, contravariant types, and bivariant types (generally called variant parametric types) by attaching a variance annotation to a type argument. On the other hand, the type system prohibits certain method/field accesses, according to variance annotations, when these accesses may otherwise make the program unsafe. By exploiting variant parametric types, a programmer can write generic code abstractions that work on a wide range of parametric types in a safe manner. For instance, a method that only reads the elements of a container of numbers can be easily modified so as to accept containers of integers, floating-point numbers, or any subtype of the number type.Technical subtleties in typing for the proposed mechanism are addressed in terms of an intuitive correspondence between variant parametric and bounded existential types. Then, for a rigorous argument of correctness of the proposed typing rules, we extend Featherweight GJ---an existing formal core calculus for Java with generics---with variant parametric types and prove type soundness.
}}

@incollection{Igarashi06b,
	Affiliation = {Kyoto University Graduate School of Informatics Yoshida-Honmachi, Sakyo-ku Kyoto 606-8501 Japan},
	Author = {Igarashi, Atsushi and Viroli, Mirko},
	Booktitle = {ECOOP 2002 --- Object-Oriented Programming},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1007/3-540-47993-7_19},
	Editor = {Magnusson, Boris},
	Isbn = {978-3-540-43759-8},
	Keywords = {type system},
	Pages = {143-167},
	Publisher = {Springer Berlin / Heidelberg},
	Series = {Lecture Notes in Computer Science},
	Title = {On Variance-Based Subtyping for Parametric Types},
	Volume = {2374},
	Year = {2006},
	Abstract = {We develop the mechanism of variant parametric types , inspired by structural virtual types by Thorup and Torgersen, as a means to enhance synergy between parametric and inclusive polymorphism in object-oriented languages. Variant parametric types are used to control both subtyping between different instantiations of one generic class and the visibility of their fields and methods. On one hand, one parametric class can be used as either covariant, contravariant, or bivariant by attaching a variance annotation---which can be either +, -, or *, respectively---to a type argument. On the other hand, the type system prohibits certain method/field accesses through variant parametric types, when those accesses can otherwise make the program unsafe. By exploiting variant parametric types, a programmer can write generic code abstractions working on a wide range of parametric types in a safe way. For instance, a method that only reads the elements of a container of strings can be easily modified so that it can accept containers of any subtype of string. The theoretical issues are studied by extending Featherweight GJ---an existing core calculus for Java with generics---with variant parametric types. By exploiting the intuitive connection to bounded existential types, we develop a sound type system for the extended calculus.}}

@inproceedings{Igarashi06c,
	Acmid = {1141610},
	Address = {New York, NY, USA},
	Author = {Igarashi, Atsushi and Nagira, Hideshi},
	Booktitle = {Proceedings of the 2006 ACM symposium on Applied computing},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1145/1141277.1141610},
	Isbn = {1-59593-108-2},
	Keywords = {language design; type system},
	Location = {Dijon, France},
	Numpages = {7},
	Pages = {1435--1441},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Union types for object-oriented programming},
	Year = {2006},
	Abstract = {We propose union types for statically typed class-based object-oriented languages as a means to enhance the flexibility of subtyping. As its name suggests, a union type can be considered a set union of instances of several types and behaves as their least common supertype. It also plays the role of an interface that 'factors out' commonality of given types---fields of the same name and methods with similar signatures. Union types can be useful for implementing heterogeneous collections and for grouping independently developed classes with similar interfaces, which has been considered difficult in languages like Java. To rigorously show the safety of union types, we formalize them on top of Featherweight Java and prove that the type system is sound.
}}

@inproceedings{Igarashi99a,
	Affiliation = {Department of Computer & Information Science, University of Pennsylvania, 200 South 33rd St., Philadelphia, PA 19104, USA},
	Author = {Igarashi, Atsushi and Pierce, Benjamin},
	Booktitle = {ECOOP' 99 --- Object-Oriented Programming},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1007/3-540-48743-3_8},
	Editor = {Guerraoui, Rachid},
	Isbn = {978-3-540-66156-6},
	Keyword = {Computer Science},
	Keywords = {type system},
	Pages = {668-668},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Foundations for Virtual Types},
	Volume = {1628},
	Year = {1999},
	Abstract = {Virtual types have been proposed as a notation for generic programming in object-oriented languages---an alternative to the more familiar mechanism of parametric classes . The tradeoffs between the two mechanisms are a matter of current debate: for many examples, both appear to offer convenient (indeed almost interchangeable) solutions; in other situations, one or the other seems to be more satisfactory. However, it has proved diffcult to draw rigorous comparisons between the two approaches, partly because current proposals for virtual types vary considerably in their details, and partly because the proposals themselves are described rather informally, usually in the complicating context of full-scale language designs. Work on the foundations of object-oriented languages has already established a clear connection between parametric classes and the polymorphic functions found in familiar typed lambda-calculi. Our aim here is to explore a similar connection between virtual types and dependent records. We present, by means of examples, a straightforward model of objects with embedded type fields in a typed lambda-calculus with subtyping, type operators, fixed points, dependent functions, and dependent records with both ``bounded'' and ``manifest'' type fields (this combination of features can be viewed as a measure of the inherent complexity of virtual types). Using this model, we then discuss some of the major differences between previous proposals and show why some can be checked statically while others require run-time checks. We also investigate how the partial ``duality'' of virtual types and parametric classes can be understood in terms of translations between universal and (dependent) existential types.}}

@inproceedings{Lu06a,
	Affiliation = {Programming Languages and Compilers Group, School of Computer Science and Engineering, University of New South Wales, Sydney},
	Author = {Lu, Yi and Potter, John},
	Booktitle = {ECOOP 2006 -- Object-Oriented Programming},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Doi = {10.1007/11785477_6},
	Editor = {Thomas, Dave},
	Isbn = {978-3-540-35726-1},
	Keyword = {Computer Science},
	Keywords = {type system},
	Pages = {99-123},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {On Ownership and Accessibility},
	Volume = {4067},
	Year = {2006},
	Abstract = {Ownership types support information hiding by providing statically enforceable object encapsulation based on an ownership tree. However ownership type systems impose fixed ownership and an inflexible access policy. This paper proposes a novel type system which generalizes ownership types by separating object accessibility and reference capability. With the ability to hide owners, it provides a more flexible and useful model of object ownership.}}

@book{Pierce02a,
	Author = {Pierce, Benjamin C.},
	Date-Added = {2013-02-26 13:11:50 +0000},
	Date-Modified = {2013-02-26 13:11:50 +0000},
	Edition = {1},
	Isbn = {9780262162098},
	Keywords = {type system},
	Month = {2},
	Publisher = {The MIT Press},
	Title = {Types and Programming Languages},
	Year = {2002}}

@techreport{ECMA11b,
	Address = {Geneva, Switzerland},
	Date-Added = {2013-01-28 09:37:07 +0000},
	Date-Modified = {2013-01-28 09:47:37 +0000},
	Institution = {ISO/IEC},
	Keywords = {JavaScript},
	Month = jun,
	Number = {ECMA-327},
	Title = {{ECMAScript $3^{rd}$ Edition Compact Profile}},
	Type = {International Standard},
	Url = {http://www.ecma-international.org/publications/standards/Ecma-327.htm},
	Year = {2011}}

@techreport{ECMA05a,
	Address = {Geneva, Switzerland},
	Date-Added = {2013-01-28 09:37:05 +0000},
	Date-Modified = {2013-01-28 09:47:28 +0000},
	Institution = {ISO/IEC},
	Keywords = {JavaScript},
	Month = dec,
	Number = {ECMA-357, $2^{nd}$ Edition},
	Title = {{ECMAScript for XML (E4X) Specification}},
	Type = {International Standard},
	Url = {http://www.ecma-international.org/publications/standards/Ecma-357.htm},
	Year = {2005}}

@techreport{ECMA12a,
	Address = {Geneva, Switzerland},
	Date-Added = {2013-01-28 09:36:40 +0000},
	Date-Modified = {2013-01-28 09:47:42 +0000},
	Institution = {ISO/IEC},
	Keywords = {JavaScript},
	Month = dec,
	Number = {ECMA-402, $1^{st}$ Edition},
	Title = {{ECMAScript Internationalization API Specification}},
	Type = {International Standard},
	Url = {http://www.ecma-international.org/publications/standards/Ecma-402.htm},
	Year = {2012}}

@techreport{ECMA11a,
	Address = {Geneva, Switzerland},
	Date-Added = {2013-01-25 11:41:11 +0000},
	Date-Modified = {2013-01-28 09:48:30 +0000},
	Institution = {ISO/IEC},
	Keywords = {JavaScript},
	Month = jun,
	Number = {ECMA-262, 5.1 Edition},
	Title = {{ECMAScript Language Specification}},
	Type = {International Standard},
	Url = {http://www.ecma-international.org/publications/standards/Ecma-262.htm},
	Year = {2011}}

@inproceedings{Salcianu05a,
	Address = {Berlin, Heidelberg},
	Author = {S\u{a}lcianu, Alexandru and Rinard, Martin},
	Booktitle = {Proceedings of the 6th international conference on Verification, Model Checking, and Abstract Interpretation},
	Date-Added = {2013-01-16 10:47:35 +0000},
	Date-Modified = {2013-01-16 10:48:35 +0000},
	Doi = {10.1007/978-3-540-30579-8_14},
	Isbn = {978-3-540-24297-0},
	Pages = {199--215},
	Publisher = {Springer-Verlag},
	Title = {Purity and side effect analysis for java programs},
	Year = {2005},
	Abstract = {We present a new purity and side effect analysis for Java programs. A method is pure if it does not mutate any location that exists in the program state right before the invocation of the method. Our analysis is built on top of a combined pointer and escape analysis, and is able to determine that methods are pure even when the methods mutate the heap, provided they mutate only new objects.

Our analysis provides useful information even for impure methods. In particular, it can recognize read-only parameters (a parameter is read-only if the method does not mutate any objects transitively reachable from the parameter) and safe parameters (a parameter is safe if it is read-only and the method does not create any new externally visible heap paths to objects transitively reachable from the parameter). The analysis can also generate regular expressions that characterize the externally visible heap locations that the method mutates.

We have implemented our analysis and used it to analyze several applications. Our results show that our analysis effectively recognizes a variety of pure methods, including pure methods that allocate and mutate complex auxiliary data structures.}}

@book{Pierce05a,
	Author = {Pierce, Benjamin C.},
	Booktitle = {Advanced Topics in Types and Programming Languages},
	Date-Added = {2013-01-16 10:44:51 +0000},
	Date-Modified = {2013-01-16 10:46:09 +0000},
	Editor = {Pierce, Benjamin C.},
	Isbn = {0-262-16228-8},
	Publisher = {MIT Press},
	Title = {Advanced Topics in Types and Programming Languages},
	Year = {2005}}

@manual{Sun97a,
	Address = {California, US},
	Author = {{Sun Microsystems}},
	Booktitle = {Java Code Conventions},
	Date-Added = {2012-12-11 09:04:10 +0000},
	Date-Modified = {2012-12-11 09:06:13 +0000},
	Month = sep,
	Organization = {Sun Microsystems},
	Title = {Java Code Conventions},
	Url = {http://www.oracle.com/technetwork/java/codeconventions-150003.pdf},
	Year = {1997}}

@book{Gosling12a,
	Author = {Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad and Buckley, Alex},
	Booktitle = {The Java Language Specification. Java SE 7 Edition},
	Date-Added = {2012-12-11 09:01:17 +0000},
	Date-Modified = {2012-12-11 09:03:51 +0000},
	Month = jul,
	Number = {JSR-000901},
	Publisher = {Oracle},
	Title = {The Java Language Specification. Java SE 7 Edition},
	Url = {http://docs.oracle.com/javase/specs/jls/se7/jls7.pdf},
	Year = {2012}}

@article{Kline05a,
	Address = {Duluth, MN, USA},
	Author = {Kline, Rex Bryan and Seffah, Ahmed},
	Date-Added = {2012-11-06 09:24:56 +0000},
	Date-Modified = {2012-11-06 09:25:11 +0000},
	Doi = {10.1016/j.ijhcs.2005.05.002},
	Issn = {1071-5819},
	Journal = {Int. J. Hum.-Comput. Stud.},
	Keywords = {CASE tools, integrated development environment (IDE), software development environment, usability, user interfaces, user-centered design},
	Month = dec,
	Number = {6},
	Pages = {607--627},
	Publisher = {Academic Press, Inc.},
	Title = {Evaluation of integrated software development environments: challenges and results from three empirical studies},
	Url = {https://doi.org/10.1016/j.ijhcs.2005.05.002},
	Volume = {63},
	Year = {2005}}

@webpage{JooseProject,
	Date-Added = {2013-03-21 15:51:53 +0000},
	Date-Modified = {2013-04-18 12:57:48 +0000},
	Key = {Joose},
	Lastchecked = {2013-03-21},
	Title = {{‎joose.github.com/Joose/doc/html/Joose/Manual.html, Project Website}},
	Type = {URL},
	Url = {http://joose.github.com/Joose/doc/html/Joose/Manual.html}}

@webpage{Closure,
	Date-Added = {2013-03-21 15:55:22 +0000},
	Date-Modified = {2013-03-21 15:55:22 +0000},
	Key = {Closure},
	Lastchecked = {2013-03-21},
	Title = {{Closure Tools --- Google Developers, Project Website}},
	Type = {URL},
	Url = {https://developers.google.com/closure/}}

@webpage{JSDoc,
	Date-Added = {2013-04-05 14:10:16 +0000},
	Date-Modified = {2013-04-05 14:10:16 +0000},
	Key = {JSDoc},
	Lastchecked = {2013-04-05},
	Title = {{jsdoc-toolkit - A documentation generator for JavaScript. - Google Project Hosting, Project Website}},
	Type = {URL},
	Url = {https://code.google.com/p/jsdoc-toolkit/}}

@webpage{MavenDependencies,
	Date-Added = {2013-04-12 14:10:16 +0000},
	Date-Modified = {2013-04-12 14:10:16 +0000},
	Key = {MavenDependencies},
	Lastchecked = {2013-04-12},
	Title = {{http://maven.apache.org/guides/introduction/introduction-to-dependency-mechanism.html, Introduction to the Dependency Mechanism}},
	Type = {URL},
	Url = {http://maven.apache.org/guides/introduction/introduction-to-dependency-mechanism.html}}

@webpage{Xtext,
	Date-Added = {2013-04-25 12:04:51 +0000},
	Date-Modified = {2013-04-25 12:05:11 +0000},
	Key = {Xtext},
	Lastchecked = {2013-04-25},
	Title = {{Xtext, Project Website}},
	Type = {URL},
	Url = {http://www.eclipse.org/Xtext/}}

@webpage{JOTWildcards,
	Date-Added = {2013-05-08 16:57:00 +0000},
	Date-Modified = {2013-05-08 16:57:00 +0000},
	Key = {JOTWildcards},
	Lastchecked = {2013-05-08},
	Title = {{Adding Wildcards to the Java Programming Language}},
	Type = {URL},
	Url = {http://www.jot.fm/issues/issue_2004_12/article5/article5.pdf}}

@webpage{ECMAWiki,
	Date-Added = {2013-05-27 14:49:31 +0000},
	Date-Modified = {2013-06-27 09:44:56 +0000},
	Key = {ECMAWiki},
	Lastchecked = {2013-05-27},
	Rating = {3},
	Title = {EcmaScript Wiki},
	Type = {URL},
	Url = {http://wiki.ecmascript.org/}}

@webpage{ES5ModuleTranspiler,
	Date-Added = {2013-07-22 13:00:04 +0000},
	Date-Modified = {2013-07-22 13:00:04 +0000},
	Key = {ES5ModuleTranspiler},
	Lastchecked = {2013-07-22},
	Title = {{ES6 Module Transpiler, Project Website}},
	Type = {URL},
	Url = {http://square.github.io/es6-module-transpiler/}}

@webpage{Dagger,
	Date-Added = {2015-07-14 08:12:31 +0000},
	Date-Modified = {2015-07-14 08:12:48 +0000},
	Key = {Dagger},
	Keywords = {dependency injection},
	Lastchecked = {2015-07-14},
	Title = {{Dagger, Project Website}},
	Type = {URL},
	Url = {http://square.github.io/dagger/}}

@book{Gosling13a,
	Author = {Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad and Buckley, Alex},
	Date-Added = {2015-07-14 08:17:57 +0000},
	Date-Modified = {2015-07-14 08:17:57 +0000},
	Edition = {public review (with diffs)},
	Importance = {1},
	Month = oct,
	Number = {JSR-000337},
	Publisher = {Oracle},
	Title = {The Java Language Specification. Java SE 8 Edition},
	Url = {http://download.oracle.com/otndocs/jcp/java_se-8-pr-spec/},
	Year = {2013}}
